Nuprl Lemma : inr-inherence
0,22
postcript
pdf
T
,
T'
:Type,
x
:
T'
,
a
:Atom1. AtomFree(Type;
T
)
AtomFree(Type;
T'
)
x
:
T'
>>
a
inr(
x
):
T
+
T'
>>
a
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
T
>>
a
,
t
T
,
x
:
A
.
B
(
x
)
,
Prop
Lemmas
inheres
wf
,
atom-free
wf
,
bfalse
wf
,
assert
wf
,
matters
wf
origin
T, T':Type, x:T', a:Atom1. AtomFree(Type;T) 
AtomFree(Type;T') x:T'>>a inr(x):T+T'>>a T, T':Type, x:T', a:Atom1. AtomFree(Type;T) AtomFree(Type;T') x:T'>>a inr(x):T+T'>>a x:A. B(x) Q
T
x:A. B(x)